$\forall$$T$, $I$:Type, $L$:($I$$\rightarrow$($T$ List)), $L_{2}$:$T$ List, $f$:($i$:$I$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$($i$)$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$).
\\[0ex]interleaved\_family\_occurence($T$;$I$;$L$;$L_{2}$;$f$) $\in$ Prop